Fix/simplify exception handling #3897

martin-cs · 2019-01-22T23:15:20Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

We had a half implemented good idea in parse_options_baset in which the main method would catch all of the various exceptions and do a standard "print and then exit with the right code" handling so that it didn't need to be duplicated in each binary. The first patch extends this so it really does catch all exceptions, the rest of the patches (ordered in increasing intrusiveness / objectionableness) then remove the redundant (and in many cases inconsistent) exception handling from various main program loops. One thing that isn't done is removing the block parts of the try as it results in large, kinda pointless whitespace commits. I'll do them if people want.

This makes the code reflect the comment "catch all exceptions here so that this code is not duplicated for each tool".

Using the previous commit these should increase the consistency of how exceptions are handled.

Again, these should only result in a net improvement in how exceptions are handled; return codes shouldn't change.

This does change the exit codes of goto-instrument in the case of exceptions being thrown. Doing so eliminates a long-standing anomoly where goto-instrument had a different exit code for exceptions to all of the other tools.

This changes the return value in a few exceptional cases in favour of being clearer about when an exception is thrown and simplifying the code.

This changes the return value in a few exceptional cases but is more consistent and simpler.

Removes specific handling of a few kinds of exception in favour of the general handlers in parse_options_baset. This will change the exit code in a few exceptional cases but makes the code simpler and more consistent.

tautschnig · 2019-01-23T13:28:25Z

src/util/parse_options.cpp

+  {
+    std::cerr << e.what() << '\n';
+    return CPROVER_EXIT_EXCEPTION;
+  }


Is this case actually needed? Shouldn't the cprover_exception_baset below catch all of them?

I don't think so but it was an explicit case in the code I removed so I thought that it had been separated out for a reason and that reason should be preserved.

Fair enough, but then you might add an extra commit that removes it? You've got a catch-all at the very end anyway.

I've added a commit that does this. Please merge if you are happy with this.

@martin-cs Historical note: When it was created there originally wasn't a base class, so we had separate handlers for each exception. A base class was added by vote. Also, we weren't entirely sure if all kinds of exceptions used the same exit code. Both of these situations were eventually remedied, so I don't think it's necessary anymore. This probably slipped past us when the situation changed.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 5804cb0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98315938

For ease of migration this case was kept from the calling code. However it is actually redundant and so is removed in this commit.

hannes-steffenhagen-diffblue

LGTM modulo minor comments

hannes-steffenhagen-diffblue · 2019-01-23T15:32:31Z

src/util/parse_options.cpp

+  {
+    std::cerr << e.what() << '\n';
+    return CPROVER_EXIT_EXCEPTION;
+  }


@martin-cs Historical note: When it was created there originally wasn't a base class, so we had separate handlers for each exception. A base class was added by vote. Also, we weren't entirely sure if all kinds of exceptions used the same exit code. Both of these situations were eventually remedied, so I don't think it's necessary anymore. This probably slipped past us when the situation changed.

hannes-steffenhagen-diffblue · 2019-01-23T15:34:36Z

src/util/exit_codes.h

@@ -40,7 +40,6 @@ Author: Martin Brain, [email protected]
 /// An (unanticipated) exception was thrown during computation.
 #define CPROVER_EXIT_EXCEPTION 6
 // should contemplate EX_SOFTWARE from sysexits.h
-#define CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT 11


This will lead to a change in exit code for goto-instrument. That doesn't bother me personally, but it's a change in behaviour, not sure if it needs to documented somewhere. Also, the comment above should be removed together with this #define

It is documented in the commit message.

The comment is general to all CPROVER_EXIT_EXCEPTION, not specifically this one.

hannes-steffenhagen-diffblue · 2019-01-23T15:35:46Z

src/goto-analyzer/goto_analyzer_parse_options.cpp

-  if(set_properties())
-    return CPROVER_EXIT_SET_PROPERTIES_FAILED;
+  if(cmdline.isset("property"))
+    ::set_properties(goto_model, cmdline.get_values("property"));


What does this change mean?

After removing the try block, set_properties only contained the two lines I've introduced and then return false so I inlined them.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 2212653).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98344221

kroening · 2019-01-23T17:41:08Z

Will this work at all with --json-ui, or --xml-ui? No error reporting for those anymore?

martin-cs · 2019-01-23T17:42:46Z

I think the exception text will be printed to std::err rather than message() but TBH it was a bit of a mish-mash where it would go before this patch.

kroening · 2019-01-23T17:48:14Z

That needs to be sorted -- all UI integrations I know rely on these showing up in the JSON.

kroening · 2019-01-23T17:48:39Z

(We should have had a test...)

Error-reporting is important, yet undertested, as shown by #3897.

martin-cs · 2019-01-24T12:16:46Z

@kroening : I'll work on a patch to make sure the we always get the exception text to the right output channel.

It seems there are two ways of doing this : have parse_optionst inherit from messaget or have a call-back in parse_optionst for outputting messages. Do you have any preference?

martin-cs · 2019-01-24T17:03:03Z

PR to allow redirection is here : diffblue/gnat2goto#113

martin-cs requested review from chrisr-diffblue, kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners January 22, 2019 23:15

smowton approved these changes Jan 23, 2019

View reviewed changes

martin added 7 commits January 23, 2019 12:51

Add default handling for the kinds of exceptions used in CPROVER

da4cc61

This makes the code reflect the comment "catch all exceptions here so that this code is not duplicated for each tool".

Remove redundant try/catch blocks from goto-analyzer

52ceb9b

Using the previous commit these should increase the consistency of how exceptions are handled.

Remove redundant try/catch blocks from cbmc

338b155

Again, these should only result in a net improvement in how exceptions are handled; return codes shouldn't change.

Remove redundant try/catch blocks from goto-instrument

920acd8

This does change the exit codes of goto-instrument in the case of exceptions being thrown. Doing so eliminates a long-standing anomoly where goto-instrument had a different exit code for exceptions to all of the other tools.

Remove some exception handling in goto-analyzer

5c23e11

This changes the return value in a few exceptional cases in favour of being clearer about when an exception is thrown and simplifying the code.

Remove some exception handling in CBMC

461e8c7

This changes the return value in a few exceptional cases but is more consistent and simpler.

Remove some exception handling in goto-diff

5804cb0

Removes specific handling of a few kinds of exception in favour of the general handlers in parse_options_baset. This will change the exit code in a few exceptional cases but makes the code simpler and more consistent.

martin-cs force-pushed the fix/simplify-exception-handling branch from 01d3ab5 to 5804cb0 Compare January 23, 2019 12:51

tautschnig approved these changes Jan 23, 2019

View reviewed changes

tautschnig assigned peterschrammel and chrisr-diffblue Jan 23, 2019

tautschnig reviewed Jan 23, 2019

View reviewed changes

allredj reviewed Jan 23, 2019

View reviewed changes

chrisr-diffblue approved these changes Jan 23, 2019

View reviewed changes

Remove redundant case in the exception handling in parse_options.cpp

2212653

For ease of migration this case was kept from the calling code. However it is actually redundant and so is removed in this commit.

hannes-steffenhagen-diffblue approved these changes Jan 23, 2019

View reviewed changes

allredj reviewed Jan 23, 2019

View reviewed changes

tautschnig merged commit 07fa10e into diffblue:develop Jan 23, 2019

kroening pushed a commit that referenced this pull request Jan 23, 2019

add a test for error reporting when using --json-ui

26de0a2

Error-reporting is important, yet undertested, as shown by #3897.

kroening mentioned this pull request Jan 23, 2019

add a test for error reporting when using --json-ui #3902

Merged

3 tasks

kroening pushed a commit that referenced this pull request Jan 23, 2019

add two tests for error reporting when using --json-ui

c4f4a0c

Error-reporting is important, yet undertested, as shown by #3897.

kroening pushed a commit that referenced this pull request Jan 23, 2019

add two tests for error reporting when using --json-ui

34fd11a

Error-reporting is important, yet undertested, as shown by #3897.

kroening pushed a commit that referenced this pull request Jan 24, 2019

add two tests for error reporting when using --json-ui

5185c8e

Error-reporting is important, yet undertested, as shown by #3897.

kroening pushed a commit that referenced this pull request Jan 24, 2019

add two tests for error reporting when using --json-ui

2cdd3ee

Error-reporting is important, yet undertested, as shown by #3897.

martin-cs mentioned this pull request Jan 24, 2019

Fix/redirect exception handler output #3921

Closed

7 tasks

This was referenced Jan 25, 2019

Fix/redirect exception handler output 2 #3951

Closed

Fix/redirect exception handler output 3 #3952

Merged

Fix/simplify exception handling #3897

Fix/simplify exception handling #3897

Uh oh!

Conversation

martin-cs commented Jan 22, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Jan 23, 2019

Uh oh!

martin-cs commented Jan 23, 2019

Uh oh!

kroening commented Jan 23, 2019

Uh oh!

kroening commented Jan 23, 2019

Uh oh!

martin-cs commented Jan 24, 2019

Uh oh!

martin-cs commented Jan 24, 2019

Uh oh!

Uh oh!